{-
 This file is part of the Clafer to Alloy Translator (clafer2alloy).

 Copyright (C) 2010 Kacper Bak <http://gsd.uwaterloo.ca/kbak>

 clafer2alloy is free software: you can redistribute it and/or modify
 it under the terms of the GNU Lesser General Public License as published by
 the Free Software Foundation, either version 3 of the License, or
 (at your option) any later version.

 clafer2alloy is distributed in the hope that it will be useful,
 but WITHOUT ANY WARRANTY; without even the implied warranty of
 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 GNU Lesser General Public License for more details.

 You should have received a copy of the GNU Lesser General Public License
 along with clafer2alloy. (See files COPYING and COPYING.LESSER.)  If not,
 see <http://www.gnu.org/licenses/>.
-}
module Desugarer where

-- desugars: enums, add default super, cardinalities, cardinalities for
-- subclafers, arrows in navigation, empty subclafers, clafer use

import Absclafer2alloy
import Common
import AlloyCode
import Monad
import List

-- -----------------------------------------------------------------------------
-- environment carries parent's group cardinality
data DEnv = DEnv GCard


desugarModule :: Module -> Module
desugarModule x = case x of
  Module declarations  ->
    Module $ map desugarDeclaration $ declarations >>= desugarEnums


-- desugars enumeration to abstract and global singleton features
desugarEnums :: Declaration -> [Declaration]
desugarEnums x = case x of
  EnumDecl ident enumids  -> absEnum : map (mkEnum ident) enumids
    where
    absEnum = AbsClaferDecl GCardEmpty ident SuperEmpty AttrEmpty
              ElementsEmpty
  _ -> [x]


mkEnum :: Ident -> EnumId -> Declaration
mkEnum superid (EnumIdIdent ident) = ClaferDecl $ Clafer GCardEmpty ident
  (Super $ Name [] superid) AttrEmpty EssentialEmpty CardEmpty ElementsEmpty


-- desugars all clafers
desugarDeclaration :: Declaration -> Declaration
desugarDeclaration x = case x of
  EnumDecl ident enumids  -> error "desugared"
  AbsClaferDecl gcard ident super attr elements  ->
    AbsClaferDecl gcard ident (desugarSuper super) (desugarAttr attr)
      (desugarElements env elements)
  ClaferDecl clafer  -> ClaferDecl $ desugarClafer env clafer
  ConstDecl constraint  -> ConstDecl $ desugarConstraint constraint
  where
  env = DEnv GCardEmpty


-- desugars non-abstract clafer
desugarClafer :: DEnv -> Clafer -> Clafer
desugarClafer penv x = case x of
  Clafer gcard ident super attr essential card elements  ->
    Clafer gcard ident (desugarSuper super) (desugarAttr attr) essential
      (desugarCard penv card) (desugarElements env elements)
    where
    env = DEnv gcard


-- desugars constraint
desugarConstraint :: Constraint -> Constraint
desugarConstraint x = case x of
  Constraint essential lexps  -> Constraint essential $ map desugarLExp lexps


-- desugars subclafers and constraints
desugarElements :: DEnv -> Elements -> Elements
desugarElements env x = case x of
  ElementsEmpty  -> Elements []
  Elements elements  -> Elements $ map (desugarElement env) elements


-- desugars single subclafer or constraint
desugarElement :: DEnv -> Element -> Element
desugarElement env x = case x of
  Subclafer clafer  -> Subclafer $ desugarClafer env clafer
  ClaferUse name essential card elements -> Subclafer $ Clafer GCardEmpty
    (Ident $ snd $ transName name) (Super name) AttrEmpty essential
    (desugarCard env card) (desugarElements env elements)
  Subconstraint constraint  -> Subconstraint $ desugarConstraint constraint


-- -----------------------------------------------------------------------------
-- sets default base clafer if there is none
desugarSuper :: Super -> Super
desugarSuper x = case x of
  SuperEmpty  ->  Super $ Name [] $ Ident baseClafer
  SuperColon name -> Super name
  Super name  -> x


-- desugars nav in attribute
desugarAttr :: Attr -> Attr
desugarAttr x = case x of
  AttrEmpty  -> x
  Attr modids nav  -> AttrSExp modids $ desugarSExp $ navToSExp nav


navToSExp :: Nav -> SExp
navToSExp x = case x of
  NavJoin nav0 nav  -> SExpJoin (navToSExp nav0) (navToSExp nav)
  NavArrow nav0 nav  -> navToSExp $ NavJoin
    (NavJoin nav0 (NavIdent $ Ident attrField)) nav
  NavIdent ident  -> SExpIdent ident


-- desugars cardinality if parent's group cardinality is "xor" or "or"
desugarCard :: DEnv -> Card -> Card
desugarCard (DEnv gcard) x = case x of
  CardEmpty  -> CardInterval $ NCard m $ ExIntegerNum n
    where
    (m, n) = case gcard of 
               GCardXor -> (0, 1)
               GCardOr  -> (0, 1)
               GCardMux -> (0, 1)
               GCardOpt -> (0, 1)
               _        -> (1, 1)
  CardLone  ->  CardInterval $ NCard 0 $ ExIntegerNum 1
  CardSome  ->  CardInterval $ NCard 1 ExIntegerAst
  CardAny  ->   CardInterval $ NCard 0 ExIntegerAst
  CardInterval ncard  -> x

-- -----------------------------------------------------------------------------
-- desugars nav in logical expressions
desugarLExp :: LExp -> LExp
desugarLExp x = case x of
  EIff lexp0 iff lexp  -> EIff (desugarLExp lexp0) iff (desugarLExp lexp)
  EImplies lexp0 implies lexp  ->
    EImplies (desugarLExp lexp0) implies (desugarLExp lexp)
  EImpliesElse lexp0 implies lexp1 lexp  -> EImpliesElse (desugarLExp lexp0)
    implies (desugarLExp lexp1) (desugarLExp lexp)
  EOr lexp0 or lexp    -> EOr  (desugarLExp lexp0) or  (desugarLExp lexp)
  EXor lexp0 xor lexp  -> EXor (desugarLExp lexp0) xor (desugarLExp lexp)
  EAnd lexp0 and lexp  -> EAnd (desugarLExp lexp0) and (desugarLExp lexp)
  ENeg neg lexp        -> ENeg neg $ desugarLExp lexp
  ETerm term           -> ETerm $ desugarTerm term


-- desugars nav in terms
desugarTerm :: Term -> Term
desugarTerm x = case x of
  TermCmpExp cmpexp  -> TermCmpExp $ desugarCmpExp cmpexp
  TermSet sexp  -> desugarTerm $ TermQuantSet QuantSome sexp
  TermQuantSet quant sexp -> TermQuantSet quant (desugarSExp sexp)
  TermQuantDeclExp decls lexp ->
    TermQuantDeclExp (map desugarDecl decls) (desugarLExp lexp)


-- desugars nav in the expressions
desugarCmpExp :: CmpExp -> CmpExp
desugarCmpExp x = case x of
  ELt exp0 exp  -> ELt  (desugarExp exp0) (desugarExp exp)
  EGt exp0 exp  -> EGt  (desugarExp exp0) (desugarExp exp)
  EREq exp0 exp -> EREq (desugarExp exp0) (desugarExp exp)
  EEq exp0 exp  -> EEq  (desugarExp exp0) (desugarExp exp)
  ELte exp0 exp -> ELte (desugarExp exp0) (desugarExp exp)
  EGte exp0 exp -> EGte (desugarExp exp0) (desugarExp exp)
  ENeq exp0 exp -> ENeq (desugarExp exp0) (desugarExp exp)
  ERNeq exp0 exp -> ERNeq (desugarExp exp0) (desugarExp exp)
  EIn exp0 exp  -> EIn  (desugarExp exp0) (desugarExp exp)
  ENin exp0 exp -> ENin (desugarExp exp0) (desugarExp exp)


-- desugars nav in espression
desugarExp :: Exp -> Exp
desugarExp x = case x of
  ESetExp sexp  -> ESetExp $ desugarSExp sexp
  ENumExp aexp -> ENumExp $ desugarAExp aexp
  EStrExp strexp -> EStrExp $ desugarStrExp strexp


-- desugars arrow in sexp
desugarSExp :: SExp -> SExp
desugarSExp x = case x of
  SExpUnion sexp0 sexp -> SExpUnion (desugarSExp sexp0) (desugarSExp sexp)
  SExpIntersection sexp0 sexp  -> SExpIntersection (desugarSExp sexp0) (desugarSExp sexp)
  SExpDomain sexp0 sexp  -> SExpDomain (desugarSExp sexp0) (desugarSExp sexp)
  SExpRange sexp0 sexp  -> SExpRange (desugarSExp sexp0) (desugarSExp sexp)
  SExpJoin sexp0 sexp  -> SExpJoin (desugarSExp sexp0) (desugarSExp sexp)
  SExpArrow sexp0 sexp  -> desugarSExp $ SExpJoin
    (SExpJoin sexp0 (SExpIdent (Ident attrField))) sexp
  SExpIdent ident  -> SExpRIdent ident False


-- desugars decl
desugarDecl :: Decl -> Decl
desugarDecl x = case x of
  Decl quant disj locids sexp -> Decl quant disj locids $ desugarSExp sexp


-- desugars arrow in sexp
desugarAExp :: AExp -> AExp
desugarAExp x = case x of
  EAdd aexp0 aexp -> x
  ESub aexp0 aexp -> x
  EMul aexp0 aexp -> x
  EUmn aexp       -> x
  ECSetExp sexp   -> ECSetExp $ desugarSExp sexp
  EInt n -> x

-- desugars string concatenation
desugarStrExp :: StrExp -> StrExp
desugarStrExp x = case x of
  EConc strexp0 strexp -> EStr $ str0 ++ str
    where
    EStr str0 = desugarStrExp strexp0
    EStr str  = desugarStrExp strexp
  EStr string -> x
